ds:x:Id fp Type. xdom(ds). A=ds(x)   A  State(ds) 

latex

Definitions	, State(ds), xdom(f). v=f(x)   P(x;v), f(x)?z, if b t else f fi, Unit, P  Q, P & Q, x  dom(f), IdDeq, a:A fp B(a), x. t(x), f(x), Id, Prop, , b, A, b, P  Q, x:A. B(x), Top, t  T
Lemmas	assert wf, not wf, bnot wf, bool wf, Id wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf wf, fpf-ap wf